mcsta

Benchmark
Model:cabinets v.1 (MA)
Parameter(s)N = 3, P = 2, R = True
Property:Unavailability (steady-state-prob)
Invocation (default)
mcsta/modest mcsta cabinets.3-2-true.jani --props Unavailability -O out.txt Minimal --unsafe --es -S Memory --no-partial-results --width 5e-2 --relative-width
Execution
Walltime:63.01635217666626s
Return code:0
Note(s):Correctness of result is not checked because no reference result is available.
Log
cabinets.3-2-true.jani:model: info: cabinets.3-2-true.jani is an MA model.
cabinets.3-2-true.jani: info: Need 24 bytes per state.
cabinets.3-2-true.jani: info: Explored 4427421 states.

Peak memory usage: 1376 MB
Analysis results for cabinets.3-2-true.jani

+ State space exploration
  State size:  24 bytes
  States:      4427421
  Transitions: 5385842
  Branches:    7983998
  Rate:        74483 states/s
  Time:        59.9 s

+ Property Unavailability
  Value: 4.1892319369589805E-08
  Time:  2.3 s

  + Essential states
    Iterations:       14
    Essential states: 354294
    Transitions:      354294
    Branches:         2952450
    Time:             1.5 s

  + LongRunAverage
    Time:                   0.7242414
    Max. end components:    1
    Max. exit rate:         4.186499999999997
    Min. exit rate:         4
    Avg. exit rate:         4.1243333333294085
    Max number of actions:  0
    Min number of actions:  2147483647
    Avg. number of actions: 0

Exported results to file "/out.txt".
STDERR
The Modest Toolset (www.modestchecker.net), version v3.1.42-gb5e9d523c.